Nuprl Lemma : qless_trichot_qorder
11,40
postcript
pdf
a
,
b
:
.
a
<
b
(
a
=
b
)
b
<
a
latex
Definitions
t
T
,
t
.1
,
OGrp
,
<
+>
,
|
g
|
,
x
:
A
.
B
(
x
)
,
r
<
s
Lemmas
ocgrp
wf
,
qadd
grp
wf2
,
grp
lt
trichot
origin
a, b:
. a < b 
(a = b) b < a a, b:. a < b (a = b) b < a 
T+>x:A. B(x)